(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
breadth(@breadth@1, @breadth@2) → breadth#1(dequeue(@breadth@1, @breadth@2))
breadth#1(tuple#2(@queue', @elem)) → breadth#2(@elem, @queue')
breadth#2(::(@z, @_@9), @queue') → breadth#3(breadth#4(@z), @queue')
breadth#2(nil, @queue') → nil
breadth#3(tuple#2(@x, @ys), @queue') → ::(@x, breadth#5(enqueues(@ys, @queue')))
breadth#4(tuple#4(@children@3, @children@4, @children@5, @children@6)) → children(@children@3, @children@4, @children@5, @children@6)
breadth#5(tuple#2(@breadth@7, @breadth@8)) → breadth(@breadth@7, @breadth@8)
children(@a, @b, @l1, @l2) → tuple#2(tuple#2(@a, @b), children#1(@l1, @b, @l2))
children#1(::(@x, @xs), @b, @l2) → children#3(@l2, @b, @x, @xs)
children#1(nil, @b, @l2) → children#2(@l2, @b)
children#2(::(@y, @ys), @b) → ::(tuple#4(@y, @b, nil, @ys), nil)
children#2(nil, @b) → nil
children#3(::(@y, @ys), @b, @x, @xs) → ::(tuple#4(@x, @b, nil, @xs), ::(tuple#4(@x, @y, @xs, @ys), nil))
children#3(nil, @b, @x, @xs) → nil
copyover(@copyover@1, @copyover@2) → copyover#1(tuple#2(@copyover@1, @copyover@2))
copyover#1(tuple#2(@inq, @outq)) → copyover#2(@inq, @outq)
copyover#2(::(@x, @xs), @outq) → copyover(@xs, ::(@x, @outq))
copyover#2(nil, @outq) → tuple#2(nil, @outq)
dequeue(@dequeue@1, @dequeue@2) → dequeue#1(tuple#2(@dequeue@1, @dequeue@2))
dequeue#1(tuple#2(@inq, @outq)) → dequeue#2(@outq, @inq)
dequeue#2(::(@y, @ys), @inq) → tuple#2(tuple#2(@inq, @ys), ::(@y, nil))
dequeue#2(nil, @inq) → dequeue#3(@inq)
dequeue#3(::(@x, @xs)) → dequeue#4(copyover(::(@x, @xs), nil))
dequeue#3(nil) → tuple#2(tuple#2(nil, nil), nil)
dequeue#4(tuple#2(@dequeue@3, @dequeue@4)) → dequeue(@dequeue@3, @dequeue@4)
empty(@x) → tuple#2(nil, nil)
enqueue(@x, @queue) → enqueue#1(@queue, @x)
enqueue#1(tuple#2(@inq, @outq), @x) → tuple#2(::(@x, @inq), @outq)
enqueues(@l, @queue) → enqueues#1(@l, @queue)
enqueues#1(::(@x, @xs), @queue) → enqueues(@xs, enqueue(@x, @queue))
enqueues#1(nil, @queue) → @queue
startBreadth(@xs) → startBreadth#1(@xs)
startBreadth#1(::(@x, @xs)) → startBreadth#2(enqueue(tuple#4(@x, @x, @xs, @xs), empty(#unit)))
startBreadth#1(nil) → nil
startBreadth#2(tuple#2(@breadth@1, @breadth@2)) → breadth(@breadth@1, @breadth@2)
Rewrite Strategy: INNERMOST
(1) DecreasingLoopProof (EQUIVALENT transformation)
The following loop(s) give(s) rise to the lower bound Ω(n1):
The rewrite sequence
breadth(@breadth@1, ::(tuple#4(@children@31760_0, @children@41761_0, ::(@x3138_0, @xs3139_0), nil), @ys281_0)) →+ ::(tuple#2(@children@31760_0, @children@41761_0), breadth(@breadth@1, @ys281_0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@ys281_0 / ::(tuple#4(@children@31760_0, @children@41761_0, ::(@x3138_0, @xs3139_0), nil), @ys281_0)].
The result substitution is [ ].
(2) BOUNDS(n^1, INF)